CI: record & use max proof runtime#213
Merged
Merged
Conversation
ahelwer
force-pushed
the
proof-max-runtime
branch
5 times, most recently
from
348ca67 to
8ccf536
Compare
Signed-off-by: Andrew Helwer <ahelwer@pm.me>
ahelwer
force-pushed
the
proof-max-runtime
branch
from
8ccf536 to
04e4315
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
It would be nice to filter the proofs based on their maximum runtime to see whether they should be run in the CI. While the manifest records HH:MM:SS "average" runtime for TLC & Apalache models, this does not make a lot of sense across so many possible machines. Thus we are trying a new approach with the proofs, where we just record the maximum number of minutes we would expect the proof to take to check on any machine that can reasonably run TLAPM. We can then easily filter on this value with
jqto avoid checking long-running proofs in the CI. This maximum time parameter is passed to the bashtimeoutcommand which will fail the CI if checking the proof exceeds the given number of minutes.@lemmy suggested just having a
check_in_ciflag in the manifest instead, which I did consider, but I think probably the CI here would want to run a greater set of proofs than the CI in the tlaplus/tlapm repo so would like to support filtering based on runtime in this way. In general I think it also seems like a better architecture to not tie manifest fields so closely to whatever tool would want to consume them.If this maxRuntimeMinutes approach is found to be a decent idea then probably we can change the model-checking process to switch to it as well.
Ref tlaplus/tlapm#273 #171